(declare-fun s () String)
(declare-fun t () String)
(assert (str.in_re (str.replace t s t) (str.to_re "AN")))
(check-sat)
(declare-fun s () (Seq Int))
(declare-fun i () Int)
(assert (xor true (seq.prefixof s (seq.unit i))))
(check-sat)
(declare-fun a () String)
(declare-fun b () String)
(assert (= "Az" (str.replace_all a b "")))
(assert (not (str.prefixof b "")))
(check-sat)
